﻿// Jinx AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System;
using System.Collections.Generic;
using System.Linq;

namespace Formality.FormalSystem
{
    using Stringer = Func<Proposition, Proposition, StringingStyle, string>;
    using Core;

    public enum PropType
    {
        Function,
        Binder,
        Operator
    }

#pragma warning disable 660, 661
    public class Proposition : Tuple<string, Series<Variable>, Series<Proposition>, Stringer, PropType>
    {
        public const string F_OP = "";
        public const string PF_OP = "!";
        private Series<Rule> Rules;

        // These two constructors let us borrow part of a preexisting proposition
        public Proposition(Proposition Base, Func<Variable, Variable> VariableMap,
                            Func<Proposition, Proposition> OperandMap)
            : base
                (
                Base.Operator,
                Series.New((from v in Base.Variables select VariableMap(v)).ToArray()),
                Series.New((from op in Base.Operands select OperandMap(op)).ToArray()),
                Base.Stringer,
                Base.Type
                )
        {
        }

        public Proposition(Proposition Base, Func<Variable, Variable> VariableMap,
                            IEnumerable<Proposition> Operands)
            : base
                (
                Base.Operator,
                Series.New((from v in Base.Variables select VariableMap(v)).ToArray()),
                Series.New(Operands.ToArray()),
                Base.Stringer,
                Base.Type
                )
        {
        }

        // Function construction
        public Proposition(Variable Name, IEnumerable<Variable> Arguments)
            : base(
                F_OP, Series.New(Concat(Name, Arguments)), new Series<Proposition>(), Stringers.FunctionStringer,
                PropType.Function)
        {
        }

        public Proposition(Variable Name, params Variable[] Arguments)
            : this(Name, (IEnumerable<Variable>)Arguments)
        {
        }

        public Proposition(Variable Name, IEnumerable<Variable> Arguments, bool Predicative)
            : base(
                Predicative ? PF_OP : F_OP, 
                Series.New(Concat(Name, Arguments)), 
                new Series<Proposition>(), 
                Stringers.FunctionStringer,
                PropType.Function)
        {
        }

        // Binder construction
        public Proposition(string Operator, Variable Variable, IEnumerable<Proposition> Scopes)
            : base(
                Operator, new Series<Variable>(Variable), Series.New(Scopes), Stringers.BinderStringer, PropType.Binder
                )
        {
        }

        // Operator construction
        public Proposition(string Operator, IEnumerable<Proposition> Operands, Stringer Stringer)
            : base(Operator, new Series<Variable>(), Series.New(Operands), Stringer, PropType.Operator)
        {
        }

        public string Operator
        {
            get { return Item1; }
        }

        public Series<Variable> Variables
        {
            get { return Item2; }
        }

        public Series<Proposition> Operands
        {
            get { return Item3; }
        }

        public Stringer Stringer
        {
            get { return Item4; }
        }

        public PropType Type
        {
            get { return Item5; }
        }

        public bool IsDefinition
        {
            get { return Binary(Operators.DEFINED) || Binary(Operators.EQ); }
        }

        public bool IsGoal
        {
            get { return Operator != Operators.AXIOM && Operator != Operators.RULE && Operator != Operators.DEFINED; }
        }

        public Series<Rule> AsRules
        {
            get
            {
                if (Rules == null)
                    Rules = Series.New(ComputeRules(this));
                return Rules;
            }
        }

        public string Detailed
        {
            get { return Stringer(this, null, StringingStyle.Detailed); }
        }

        public bool Binary(string ForOperator)
        {
            return Operator == ForOperator && Operands.Length == 2;
        }

        public override string ToString()
        {
            return Stringer(this, null, StringingStyle.Default);
        }

        public static implicit operator Proposition(string Name)
        {
            return Name.Function();
        }

        private static IEnumerable<Variable> Concat(Variable Name, IEnumerable<Variable> Arguments)
        {
            yield return Name;
            foreach (var a in Arguments) yield return a;
        }

        private static IEnumerable<Rule> ComputeRules(Proposition Prop)
        {
            return ComputeRules(Prop, new List<Proposition>());
        }

        private static IEnumerable<Rule> ComputeRules(Proposition Prop, List<Proposition> Antecedents)
        {
            if (Prop.Operator == Operators.RULE)
                yield return new Rule(Prop);

            if (Prop.Operator == Operators.AXIOM)
                yield return new Rule(Prop);

            while (Prop.Binary(Operators.IMPLIES))
            {
                var Consequent = Prop.Operands[1];

                Antecedents.Add(Prop.Operands[0]);
                yield return new Rule(Series.New(Antecedents).Eval(), Consequent);

                Prop = Consequent;
            }
        }
    }
#pragma warning restore
}